T:Type, l:(T List). no_repeats(T; l)  (x,y:T. l_before(x; y; l; T)  ((x = y))) 

latex

Definitions	suptype(S; T), subtype(S; T), False, A  B, Y, t  ...$L, ge(i; j), prop{i:l}, t  T, P  Q, P  Q, x:A. B(x), sublist(T; L1; L2), ||as||, A, l_before(x; y; l; T), P  Q, no_repeats(T; l), P  Q, x:A. B(x), , lelt(i; j; k), int_seg(i; j), increasing(f; k), ff, tt, if b then t else f fi , i <z j, b, i z j, nth_tl(n;as), hd(l), guard(T), sq_type(T), l[i], tl(l), P  Q, decidable(P), Unit, ,
Lemmas	not wf, nat wf, select wf, non neg length, length cons, length nil, increasing wf, length wf1, int seg wf, le wf, decidable lt, eq int wf, ifthenelse wf, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, bnot wf, assert wf, bool wf